[Merged by Bors] - feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive by CoolRmal · Pull Request #30230 · leanprover-community/mathlib4

CoolRmal · 2025-10-05T02:37:16Z

Add some basic lemmas about the integral of a vector measure. This PR specifically focuses on the additivity of the integral.

Created with the help of Codex.

depends on: [Merged by Bors] - feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure #28499
depends on: [Merged by Bors] - feat(MeasureTheory): triangle inequality for the variation of vector measures #39103

github-actions · 2025-10-05T02:38:33Z

PR summary 0606ced125

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ add_left_measure
+ add_right_measure
+ apply_eq_zero_of_isEmpty
+ coe_finsetSum
+ eq_zero_of_isEmpty
+ finsetSum_measure
+ instance [IsEmpty α] : Subsingleton (VectorMeasure α M)
+ integral_add_cbm
+ integral_add_vectorMeasure
+ integral_congr_ae
+ integral_eq_zero_of_ae
+ integral_finsetSum
+ integral_finsetSum_cbm
+ integral_finsetSum_vectorMeasure
+ integral_neg_cbm
+ integral_neg_vectorMeasure
+ integral_of_isEmpty
+ integral_sub_cbm
+ integral_sub_vectorMeasure
+ integral_undef
+ integral_zero
+ integral_zero_cbm
+ integral_zero_vectorMeasure
+ of_le
+ setToFun_add_measure
+ setToFun_finsetSum_measure
+ setToFun_neg'
+ setToFun_sub_measure
+ sub
+ sub_measure
+ transpose_add_cbm
+ transpose_add_vectorMeasure
+ transpose_finsetSum_cbm
+ transpose_finsetSum_vectorMeasure
+ transpose_neg_cbm
+ transpose_neg_vectorMeasure
+ transpose_sub_cbm
+ transpose_sub_vectorMeasure
+ transpose_zero_cbm
+ transpose_zero_vectorMeasure
++ add_measure
++ neg

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

mathlib4-merge-conflict-bot · 2025-11-19T08:13:23Z

This pull request has conflicts, please merge master and resolve them.

@yoh-tanimoto

…measures (#39103) We show that the variation of vector measures satisfies the triangle inequality. As an application, we show that integrals are additive in vector measures and bilinear forms in #30230. Coauthored by @yoh-tanimoto. Created with the help of Codex.

mathlib-dependent-issues · 2026-05-12T08:06:18Z

This PR/issue depends on:

~~[Merged by Bors] - feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure #28499~~
~~[Merged by Bors] - feat(MeasureTheory): triangle inequality for the variation of vector measures #39103~~
By Dependent Issues (🤖). Happy coding!

CoolRmal · 2026-05-24T22:23:16Z

@sgouezel I just addressed some of the comments. I would prefer that this PR be merged and cleaned up afterwards, as I need to focus on some other projects recently and don’t want to slow down the progress on integration by parts. If cleaning up this PR turns out to be overly complicated, I can also close it.

CoolRmal · 2026-05-24T22:24:27Z

-awaiting-author

sgouezel · 2026-05-25T09:09:38Z

Then I'd say let's merge this in, and then I'll do a cleanup PR. This makes sense as your PR is already in an excellent shape. @EtienneC30, does it seems reasonable to you?

EtienneC30

Thanks, I think it's ready to go!
maintainer delegate

EtienneC30 · 2026-05-25T09:57:50Z

 noncomputable def integral (μ : VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G) : G :=
  if _ : CompleteSpace G then
  setToFun (μ.transpose B).variation (μ.transpose B)
    (dominatedFinMeasAdditive_cbmApplyMeasure μ B) f
  else 0


I was going to suggest you add a lemma

lemma integral_def [hG : CompleteSpace G] : ∫ᵛ x, f x ∂[B; μ] = setToFun (μ.transpose B).variation (μ.transpose B) (dominatedFinMeasAdditive_cbmApplyMeasure μ B) f := by simp [integral, hG]; rfl

to use simp only [integral_def] in proofs but this actually fails because cbmApplyMeasure is not exposed so is not unfolded. Looks to me like the definition should replace (µ.transpose B) with (cbmApplyMeasure µ B) and your lemmas about transpose should actually be about cbmApplyMeasure. This is not really a problem but I thought I'd mention it.

github-actions · 2026-05-25T10:05:26Z

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

sgouezel · 2026-05-25T10:23:15Z

bors d+

mathlib-bors · 2026-05-25T10:23:17Z

✌️ CoolRmal can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

CoolRmal · 2026-05-26T14:56:39Z

bors r+

… a vector measure is additive (#30230) Add some basic lemmas about the integral of a vector measure. This PR specifically focuses on the additivity of the integral. Created with the help of Codex.

mathlib-bors · 2026-05-26T15:50:49Z

Pull request successfully merged into master.

Build succeeded:

… a vector measure is additive (leanprover-community#30230) Add some basic lemmas about the integral of a vector measure. This PR specifically focuses on the additivity of the integral. Created with the help of Codex.

github-actions Bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory labels Oct 5, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 5, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

yoh-tanimoto mentioned this pull request Apr 16, 2026

[Merged by Bors] - feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure #28499

Closed

1 task

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 5, 2026

mathlib-dependent-issues Bot deleted a comment from mathlib4-dependent-issues-bot May 5, 2026

CoolRmal closed this May 7, 2026

CoolRmal force-pushed the VectorMeasureIntegral branch from 8be6a9b to 7948ce3 Compare May 7, 2026 20:15

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 7, 2026

CoolRmal added 2 commits May 8, 2026 09:09

update

df68816

update

b3d214d

CoolRmal reopened this May 8, 2026

CoolRmal added 5 commits May 8, 2026 15:23

Update FinMeasAdditive.lean

82d428f

update

c73ee93

Update Basic.lean

fa70a41

Update Integral.lean

caa8ff8

Update Basic.lean

8a9255b

CoolRmal changed the title ~~feat(MeasureTheory): Basic properties of the integral against a vector measure with a bilinear form.~~ feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive May 9, 2026

finishes proof

876d734

CoolRmal marked this pull request as ready for review May 9, 2026 02:49

Merge branch 'master' into VectorMeasureIntegral

030f3e4

CoolRmal mentioned this pull request May 9, 2026

[Merged by Bors] - feat(MeasureTheory): triangle inequality for the variation of vector measures #39103

Closed

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 9, 2026

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 12, 2026

Merge branch 'master' into VectorMeasureIntegral

4d4f109

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 24, 2026

EtienneC30 reviewed May 25, 2026

View reviewed changes

EtienneC30 added the awaiting-author A reviewer has asked the author a question or requested changes. label May 25, 2026

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 25, 2026

CoolRmal and others added 9 commits May 26, 2026 10:17

Update Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

dc41fb6

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Update Mathlib/MeasureTheory/VectorMeasure/Integral.lean

ab8b3de

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Update Mathlib/MeasureTheory/VectorMeasure/Integral.lean

4d206f0

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Update Mathlib/MeasureTheory/VectorMeasure/Integral.lean

6bd29bf

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Update Mathlib/MeasureTheory/VectorMeasure/Integral.lean

0c19b00

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Update Mathlib/MeasureTheory/VectorMeasure/Integral.lean

69b3ac3

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Update Mathlib/MeasureTheory/VectorMeasure/Integral.lean

de37743

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

Update Mathlib/MeasureTheory/VectorMeasure/Integral.lean

b7058ab

Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>

fix

0606ced

mathlib-bors Bot changed the title ~~feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive~~ [Merged by Bors] - feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive May 26, 2026

mathlib-bors Bot closed this May 26, 2026

CoolRmal deleted the VectorMeasureIntegral branch May 26, 2026 16:15

Uh oh!

Conversation

CoolRmal commented Oct 5, 2025 • edited by RemyDegenne Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Oct 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0606ced125

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

mathlib-dependent-issues Bot commented May 12, 2026

Uh oh!

CoolRmal commented May 24, 2026

Uh oh!

CoolRmal commented May 24, 2026

Uh oh!

sgouezel commented May 25, 2026

Uh oh!

EtienneC30 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

EtienneC30 May 25, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented May 25, 2026

Uh oh!

sgouezel commented May 25, 2026

Uh oh!

mathlib-bors Bot commented May 25, 2026

Uh oh!

CoolRmal commented May 26, 2026

Uh oh!

mathlib-bors Bot commented May 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

CoolRmal commented Oct 5, 2025 •

edited by RemyDegenne

Loading

github-actions Bot commented Oct 5, 2025 •

edited

Loading